package joc.nextgen;

import static joc.nextgen.JOC.post;
import static joc.nextgen.JOC.pre;
import static joc.nextgen.JOC.unchanged;

public class TimeOfDayContract extends TimeOfDay {
	@Invariant
	public void invariant() {
		assert getHour() >= 0 && getHour() <= 23;
		assert getMinute() >= 0 && getMinute() <= 59;
		assert getSecond() >= 0 && getSecond() <= 59;
	}

	@Override
	public void setHour(int hour) {
		if (pre()) {
			assert hour >= 0 && hour <= 23;
		} else {
			assert getHour() == hour;
			unchanged(getMinute(), getSecond());
		}
	}

	@Override
	public void setMinute(int minute) {
		if (pre()) {
			assert minute >= 0 && minute <= 59;
		}
		if (post()) {
			assert getMinute() == minute;
			unchanged(getSecond(), getHour());
		}
	}

	@Override
	public void setSecond(int second) {
		if (pre()) {
			assert second >= 0 && second <= 59;
		}
		if (post()) {
			assert getSecond() == second;
			unchanged(getMinute(), getHour());
		}
	}

}